package org.stragma.apply.modules

import org.kiama.rewriting._
import org.kiama.rewriting.Rewriter.{all,attempt,debug,fail,id,not,rulefs,Strategy,Term,where,topdown}

import org.stragma.apply.signatures.Apply._
import org.stragma.apply.signatures.ApplyExtensions._

import org.stragma.apply.signatures.Options._
import org.stragma.apply.signatures.Conversions._
import org.stragma.apply.modules._
import org.stragma.apply.modules.ApplyStrategies._
import org.stragma.apply.modules.Options._
import org.stragma.apply.util.LogicalOperators._

/**
 *	ImageMatrix is a port of the ImageMatrix Apply program
 */
object ImageMatrix {
	
	/**
	 *	VarExtension extends Var. It has been created to introduce a psuedo concrete like
	 *	syntax. This has been achieved through the use of operator methods
	 */
	private val row = new VarExtension("row")
	private val column = new VarExtension("column")
	private val width = new VarExtension("width")
	private val height = new VarExtension("height")
	private val app_index = new VarExtension("app_index")
	private val app_size = new VarExtension("app_size")
	
	private val _0 = Int("0")
	private val _1 = Int("1")
	
	/*
	 * This helper method execute simplify "n" number of times
	 */
	def Apply_Image_matrixHelper ( term : Term, n : scala.Int ) : Term = {
		var result : Term = scala.None
		for(i <- 0 until n) {
			result = (Apply_Image_matrix(term)).get
			
			// Added the println to mimic the way strategoxt.jar works
			println(result)
		}
		
		result
	}
	
	/*
	 * This helper method executes normaliseTest n times and returns
	 * the very last result to the caller
	 */
	def Apply_Image_matrixHelper ( file : String, n : scala.Int ) : Term = {
		val iTerm = loadTermFromFile (file)
		Apply_Image_matrixHelper (iTerm, n)
	}
	
	/**
	 *	Port of the primary Image_matrix strategy. Note that this strategy
	 * 	has not support for generating test code
	 */
	def Apply_Image_matrix = 
		topdown(attempt(declare_variables)) <*
		attempt(get_option(Width_512()) <* make_fixed_width_cases(List(Int("512")))) 
		attempt(not(get_option(Loop_nosingle())) <* topdown(attempt(FixLoopSinglePixel))) <*
		fix_loop_window <*
		topdown(attempt(FixDefined)) <*
		fix_windows <* topdown(attempt(FixDefined))
		
	/**
	 *	Port of declare-variables from Apply Image_Matrix Stratego program
	 */
	def declare_variables = 
		rulefs {
			// declare-variables =
		  	//	?Procedure(name, args, decs, stmts, ename)
		  	//		; !Procedure(name, Arguments([args | [ |[ height, width : in integer ]| ] ]),
		  	//      	[decs | [ |[ row, column, app_index, app_size : integer; ]| ] ], stmts, ename)
			case Procedure(name, args, decs, stmts, ename) =>
				
				// Add new arguments
				val newArg = In(VarList(height :: width :: Nil), Type(Integer()))
				val argsOrg = args.asInstanceOf[Arguments]
				
				// Add new declarations
				val newDecl = Declaration(VarList(row :: column :: app_index :: app_size :: Nil), Integer())
				val declOrg = decs.asInstanceOf[Declarations]
				
				Procedure(name, 
					Arguments(argsOrg.arg0 ::: List(newArg)), 
					Declarations(declOrg.arg0 ::: List(newDecl)), 
					stmts, 
					ename)
		}
	
	/**
	 *	Strategty generate-test-code will not be ported as it is not going to be used in the context
	 *  of this project, in addition it uses native calls from Stratego to C
	 */
	
	/**
	 *	Port of the strategy fix-loop-window
	 */
	def fix_loop_window = 
		(get_option(Loop_1()) <* not(get_option(Loop_index())) <* topdown(attempt(FixLoop1NoIndex))) <+ 
		(get_option(Loop_2()) <* (get_option(Loop_index()) <* topdown(attempt(FixLoop2Index)) <+ topdown(attempt(FixLoop2NoIndex)))) <+ 
		(get_option(Loop_10()) <* (get_option(Loop_index()) <* (get_option(Loop_block()) <* Nil <+ topdown(attempt(FixLoop10RasterIndex))) <+ (get_option(Loop_block()) <* topdown(attempt(FixLoop10BlockNoIndex)) <+ topdown(attempt(FixLoop10RasterNoIndex))))) <+ Nil
	
	def fix_windows = (get_option(Loop_index()) <* fix_windows_index) <+ fix_windows_noindex
	def fix_windows_noindex = topdown(attempt(FixWindowsNoIndexBorder <+ FixWindowsNoIndex <+ FixWindowsArg))
	def fix_windows_index = topdown(attempt(FixWindowsIndexBorder <+ FixWindowsIndex <+ FixWindowsArg))

	/**
	 *	Port of the strategy make-fixed-width-cases
	 */
	def make_fixed_width_cases(widths : List[TExp]) = topdownstopping(fixed_width_cases(widths))

	/**
	 *	Port of the strategy fixed_width_cases
	 */
	def fixed_width_cases(widths : List[TExp]) = 
		rulefs {
			case Statements(ApplyLoop(atype, e1 : Int, e2 : Int, e3 : Int, e4 : Int, s) :: Nil) =>
				fixed_width_generate(widths)
		}

	/**
	 * 	Note that the if statement generates an assertion that
	 * 	causes the generated code to exploit the fact that we have selected a particular
	 *  known value of width.
	 */
	def fixed_width_generate(widths : List[TExp]) : Strategy =
		rulefs {
			case Var("applyloop") if (widths == Nil) =>
				id
			case Var("applyloop") =>
				where ( match_width_list(Var("applyloop"))(widths) )
		}

	private def match_width_list(v : Var) = 
		rulefs {
			case h :: t =>
			
				val recastHead = h.asInstanceOf[TExp]
				val recastTail = t.asInstanceOf[List[TExp]]
			
				val rest = (fixed_width_generate(recastTail))(v)
				if (rest.isDefined) {
					IfElseExp(Equ(width, recastHead), v, rest.get.asInstanceOf[TExp])
				} else {
					id
				}
			case _ =>
				fail
		}

	/**
	 * 	Loop assertions are included directly so that this simple loop form can be used
	 *	with limited optimisation
	 */
	def FixLoop1NoIndex =
		rulefs {
			/**
				FixLoop1NoIndex :
		    		|[ @apply ~type window (i1..i2,j1..j2) loop ~s end loop; ]| ->
		    		|[ 
		       			for row in 0..height-1 loop
		         			for column in 0..width-1 loop
		           				assert row >= 0 and row <= height-1;
		           				assert column >= 0 and column <= width-1;
		           				~s
		         			end loop;
		       			end loop;
		    		]|
		 	 */
			case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>
						
				val outer_for = 
					For(row, _0, height - _1, 
						Statements(
							For(column, _0, width - _1, 
								Statements(
									assert ( (row >= _0) and (row <= height - _1) ) :: 
									assert ( (column >= _0) and (column <= width - _1) ) :: 
									s)) :: 
									Nil))
	
				Statements(outer_for :: Nil)
		}

	/**
	 * In the single loop solution, we need to specifically apply the appropriate
  	 * fix windows rules to the loop body since the options do not determine
  	 * whether an index variable is used or not.
	 */
	def FixLoopSinglePixel = 
		rulefs {
			/**
				FixLoopSinglePixel :
		      |[ @apply @index window (0..0,0..0) loop ~s end loop; ]| ->
		    		|[ app_size := width * height;
		    		   @cfor app_index @:= 0; app_index < app_size; app_index @:= app_index + 1 loop
		    		     ~q
		    		   end loop;
		    	]|  where <fix-windows-index>s => q
			 */
			case Statements(ApplyLoop(Index(), Int("0"), Int("0"), Int("0"), Int("0"), s) :: Nil) =>
			
				val sMod = ((where(fix_windows_index)(s)).get).asInstanceOf[TStatements]
				
				Statements( 
					(app_size := (width * height)) :: 
					CFor(app_index @:= _0, 
						app_index < (width * height), 
						app_index @:= (app_index + _1), 
						sMod) :: 
					Nil )
			
			/**
				FixLoopSinglePixel :
				|[ @apply @rowcolumn window (0..0,0..0) loop ~s end loop; ]| ->
			  |[ @cfor row @:= 0; row < height; row @:= row + 1 loop
					    @cfor column @:= 0, app_index @:= 0; column < width; column @:= column + 1, app_index @:= app_index + 1 loop
					       ~q
			      	 end loop;
					end loop;
				]|  where <fix-windows-noindex>s => q
			 */
			case Statements(ApplyLoop(RowColumn(), Int("0"), Int("0"), Int("0"), Int("0"), s) :: Nil) =>

				val stmtsMod = ((where(fix_windows_noindex)(s)).get).asInstanceOf[TStatements]
				
				val inner_for = CFor1( (column @:= _0) :: (app_index @:= _0), 
									column < width, 
									(column @:= (column + _1)) :: (app_index @:= (app_index + _1)), 
									stmtsMod)
									
				val outer_for = CFor(row @:= _0, 
									row < height, 
									row @:= (row + _1), 
									Statements( inner_for :: Nil ))

				Statements( outer_for :: Nil )
		}

	/**
	 *	There is apparently a bug in the /...\ notation that causes the if-derived assertion row >= -i1
	 *	to withdraw the assertion row >= 0 when the if exits.  Work around: explicitly assert bounds on
	 *	row inside the column loop.
	 */
	def FixLoop2Index =
		rulefs {
			/*
				FixLoop2Index :
			    |[ @apply ~looptype window (i1..i2,j1..j2) loop ~s end loop; ]| -> 
			    |[ app_index := 0;
			         for row in 0..height-1 loop
			           @cfor column @:= 0; column <= width-1; loop
			             assert column >= 0 and column <= width - 1;
					 				 assert row >= 0 and row <= height-1;
			             ~s
			             if column = -j1-1 and row >= -i1 and row < height - i2 then
			               column := column + width - j2 + j1 + 1;
			               app_index := app_index + width - j2 + j1 + 1;
			             else
			               column := column + 1;
			               app_index := app_index + 1;
			             end if;
			           end loop;
			         end loop;
			       app_index := -i1 * width - j1;
			         for row in -i1..height-i2-1 loop
			           for column in -j1..width-j2-1 loop
			             ~s
			             app_index := app_index + 1;
			           end loop;
			           app_index := app_index -i1 + i2;
			         end loop;
			    ]|   where(<debug> ["extreme window dimensions: ", i1, i2, j1 ,j2])
			 */
			case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>

				val assert_column = assert ( (column >= _0) and (column <= (width - _1)) )
				val assert_row = assert ( (row >= _0) and (row <= (height - _1)) )
				
				val assign_column_onTrue = column := (column + (width - (j2 + (j1 + _1))))
				val assign_app_index_onTrue = app_index := (app_index + (width - (j2 + (j1 + _1))))
				
				val assign_column_onFalse = column := (column + _1)
				val assign_app_index_onFalse = app_index := (app_index + _1)

				val if_cond1 = column == (Neg(j1) - _1)
				val if_cond2 = row >= Neg(i1)
				val if_cond3 = row < (height - i2)
				val if_else_stmt = IfElse(if_cond1 and (if_cond2 and if_cond3),
									Statements( assign_column_onTrue :: assign_app_index_onTrue :: Nil ),
									Statements( assign_column_onFalse :: assign_app_index_onFalse :: Nil ))
				
				val for_stmts1 = Statements( assert_column ::: assert_row ::: s ::: if_else_stmt ) 
				val cfor = CFor(column @:= _0, column <= (width - _1), None(), for_stmts1)
				
				val for1 = For(row, _0, height - _1, Statements( cfor :: Nil ))
				val update_app_index = app_index := ((Neg(i1) * width) - j1)
				
				val for2 = For(column, 
							Neg(j1), 
							width - (j2 - _1), 
							Statements( s ::: assign_app_index_onFalse ))			
							
				val for3 = For(row, 
							Neg(i1), 
							height - (j2 - _1), 
							Statements( for2 :: Nil ))
				
				Statements( (app_index := _0) :: for1 :: for3 :: Nil)
		}

	def FixLoop2NoIndex = 
		rulefs {
			/*
			|[ @apply ~looptype window (i1..i2,j1..j2) loop ~s end loop; ]| -> 
    	|[ 
	         for row in 0..height-1 loop
	           @cfor column @:= 0; column <= width-1; loop
	             assert column >= 0 and column <= width - 1;
	             assert row >= 0 and row <= height-1;
	             ~s
	             if column = -j1-1 and row >= -i1 and row < height - i2 then
	               column := column + width - j2 + j1 + 1;
	             else
	               column := column + 1;
	             end if;
	           end loop;
	         end loop;
	         for row in -i1..height-i2-1 loop
	           for column in -j1..width-j2-1 loop
	             ~s
	           end loop;
	         end loop;
	    ]|   where(<debug> ["extreme window dimensions: ", i1, i2, j1 ,j2])
			*/
			case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>

				val assert_column = assert ( (column >= _0) and (column <= width - _1) )
				val assert_row = assert ( (row >= _0) and (row <= (height - _1)) )
				
				val assign_column_onTrue =  column := (column + (width - (j2 + (j1 + _1))))
				val assign_column_onFalse = column := (column + _1)

				val if_cond1 = column == (Neg(j1) - _1)
				val if_cond2 = row >= Neg(i1)
				val if_cond3 = row < (height - i2)
				val if_else_stmt = IfElse(if_cond1 and (if_cond2 and if_cond3),
									Statements( assign_column_onTrue :: Nil ),
									Statements( assign_column_onFalse :: Nil ))
				
				val for_stmts1 = Statements( assert_column ::: assert_row ::: s ::: if_else_stmt )
				
				// @:= is syntactic sugar for CAssign
				val cfor = CFor(column @:= _0, column <= (width - _1), None(), for_stmts1)
				
				val for1 = For(row, 
							_0, 
							height - _1, 
							Statements( cfor :: Nil ))
							
				val for2 = For(column, 
							Neg(j1), 
							width - (j2 - _1), 
							s)
							
				val for3 = For(row, 
							Neg(i1), 
							height - (j2 - _1), 
							Statements( for2 :: Nil ))
				
				// for2 is nested within the for3 loop
				Statements( for1 :: for3 :: Nil )
		}
		
	def FixLoop4c =
		rulefs {
			/*
				|[ @apply ~looptype window (i1..i2,j1..j2) loop ~s end loop; ]| -> 
    		|[ app_index := 0;
		       @cfor row @:= 0; row < height; row @:= row + 1 loop
		         assert row >= 0 and row < height;
		         if row < -i1 or row >= height-i2 then
		           @cfor column @:= 0; column < width; column @:= column + 1, app_index @:= app_index + 1 loop
		             ~s
		           end loop;
		         else
		           @cfor column @:= 0; column < -j1 and column < width; column @:= column + 1, app_index @:= app_index + 1 loop
		             ~s
		           end loop;
		           assert column >= -j1;
		           @cfor ; column < width-j2; column @:= column + 1, app_index @:= app_index + 1 loop
		             assert column >= -i1 and column < width-j2;
		             ~s
		           end loop;
		           assert column >= width-j2;
		           @cfor ; column < width; column @:= column + 1, app_index @:= app_index + 1 loop
		             assert column >= width-j2;
		             ~s
		           end loop;
		         end if;
		       end loop;
		    ]|   where(<debug> ["extreme window dimensions: ", i1, i2, j1 ,j2])
			 */
			case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>
			 	
				val assert_row = assert ((row >= _0) and (row < height))
				
				// @:= is an alias for CAssign
				val cfor1 = CFor1 ((column @:= _0) :: Nil, 
								column < width, 
								(column @:= (column + _1)) :: (app_index @:= (app_index + _1)), 
								s)
				
				val cfor2 = CFor1 ( (column @:= _0) :: Nil, 
								(column < Neg(j1)) and (column < width), 
								(column @:= (column + _1)) :: (app_index @:= (app_index + _1)), 
								s)
				
				val assert1 = assert ((column >= Neg(i1)) and (column < (width - j2)))
				
				val cfor3 = CFor1(Nil, 
								column < (width - j2), 
								(column @:= (column + _1)) :: (app_index @:= (app_index + _1)), 
								Statements( assert1 ::: s ))
				
				val assert2 = assert (column >= (width - j2))
				
				val cfor4 = CFor1(Nil, 
								column < width, 
								(column @:= (column + _1)) :: (app_index @:= (app_index + _1)), 
								Statements( assert2 ::: s ))
				
				val else_statements = Statements( cfor2 :: assert (column >= Neg(j1)) :: cfor3 :: assert2 :: cfor4 :: Nil )
				
				val if_else_stmt = IfElse((row < Neg(i1)) or (row >= (height - i2)), 
									Statements( cfor1 :: Nil ), 
									else_statements)
				
				val cfor = CFor(row @:= _0, 
							row < height, 
							row @:= row + _1, 
							Statements( assert_row :: if_else_stmt :: Nil ))
							
				Statements( (app_index := _0) :: cfor :: Nil)
		}

	def FixLoop6 =
		rulefs {
			/*
				|[ @apply ~looptype window (i1..i2,j1..j2) loop ~s end loop; ]| -> 
    		|[ app_index := 0;
		       if width > j2 - j1 and height > i2 - i1 then
		         for row in 0..-i1-1 loop
		           assert row < height - i2;
		           for column in 0..width-1 loop
		             ~s
		             app_index := app_index + 1;
		           end loop;
		         end loop;
		         for row in -i1..height-i2-1 loop
		           for column in 0..-j1-1 loop
		             assert column < width - j2;
		             ~s
		             app_index := app_index + 1;
		           end loop;
		           for column in -j1..width-j2-1 loop
		             ~s
		             app_index := app_index + 1;
		           end loop;
		           for column in width-j2..width-1 loop
		             assert column >= -j1;
		             ~s
		             app_index := app_index + 1;
		           end loop;
		         end loop;
		         for row in height-i2..height-1 loop
		           assert row >= -i1;
		           for column in 0..width-1 loop
		             ~s
		             app_index := app_index + 1;
		           end loop;
		         end loop;
		       else
		         for row in 0..height-1 loop
		           for column in 0..width-1 loop
		             ~s
		             app_index := app_index + 1;
		           end loop;
		         end loop;
		       end if;
		    ]|   where(<debug> ["extreme window dimensions: ", i1, i2, j1 ,j2])
			 */
			case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>
			 	
				val for1_inner = For(column, 
									_0, 
									width - _1, 
									Statements( s ::: (app_index := app_index + _1)))
									
				val for1 = For(row, 
							_0, 
							Neg(i1) - _1, 
							Statements( Assert(row < (height - i2)) :: for1_inner :: Nil ))
				
				val for2_inner1 = For(column, 
									_0, 
									Neg(j1) - _1, 
									Statements( assert (column < (width - j2)) ::: s ::: (app_index := app_index + _1)))
				
				val for2_inner2 = For(column, 
									Neg(j1), 
									width - (j2 - _1), 
									Statements( s ::: (app_index := app_index + _1)))
									
				val for2_inner3 = For(column, 
									width - j2, 
									width - _1, 
									Statements( assert (column >= Neg(j2)) ::: s ::: (app_index := app_index + _1) ))
				
				val for2 = Statements( for2_inner1 :: for2_inner2 :: for2_inner3 :: Nil )
				
				val for3_inner = For(column, 
									_0, 
									width - _1, 
									Statements( s ::: (app_index := app_index + _1)))
									
				val for3 = For(row, 
							height - i2, 
							height - _1, 
							Statements( Assert(row > Neg(i1)) :: for3_inner :: Nil ))
				
				val for4 = For(row, 
							_0, 
							height - _1, 
							Statements( for3_inner :: Nil ))
				
				val if_else_stmt = IfElse((width > (j2 -j1)) and (height > (i2 -i1)),
									Statements(List(for1) ::: for2.arg0 ::: List(for3)),
									Statements(for4 :: Nil))
				
				Statements( (app_index := _0) :: if_else_stmt :: Nil)
		}

		def FixLoop10RasterIndex = 
			rulefs {
				/*
					FixLoop10RasterIndex :
			    |[ @apply ~looptype window (i1..i2,j1..j2) loop ~s end loop; ]| -> 
			    |[ app_index := 0;
			       if width > j2 - j1 and height > i2 - i1 then
			         for row in 0..-i1-1 loop
			           assert row < height - i2;
			           for column in 0..-j1-1 loop
			             assert column < width - j2;
			             ~s
			             app_index := app_index + 1;
			           end loop;
			           for column in -j1..width-j2-1 loop
			             ~s
			             app_index := app_index + 1;
			           end loop;
			           for column in width-j2..width-1 loop
			             assert column >= -j1;
			             ~s
			             app_index := app_index + 1;
			           end loop;
			         end loop;
			         for row in -i1..height-i2-1 loop
			           for column in 0..-j1-1 loop
			             assert column < width - j2;
			             ~s
			             app_index := app_index + 1;
			           end loop;
			           for column in -j1..width-j2-1 loop
			             ~s
			             app_index := app_index + 1;
			           end loop;
			           for column in width-j2..width-1 loop
			             assert column >= -j1;
			             ~s
			             app_index := app_index + 1;
			           end loop;
			         end loop;
			         for row in height-i2..height-1 loop
			           assert row >= -i1;
			           for column in 0..-j1-1 loop
			             assert column < width - j2;
			             ~s
			             app_index := app_index + 1;
			           end loop;
			           for column in -j1..width-j2-1 loop
			             ~s
			             app_index := app_index + 1;
			           end loop;
			           for column in width-j2..width-1 loop
			             assert column >= -j1;
			             ~s
			             app_index := app_index + 1;
			           end loop;
			         end loop;
			       else
			         for row in 0..height-1 loop
			           for column in 0..width-1 loop
			             ~s
			             app_index := app_index + 1;
			           end loop;
			         end loop;
			       end if;
			    ]|   where(<debug> ["extreme window dimensions: ", i1, i2, j1 ,j2])
		*/
			case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>
				
				val for1_inner_for1 = For(column, 
										_0, 
										Neg(j1) - _1, 
										Statements( assert (column < (width - j2)) ::: s ::: (app_index := app_index + _1) ))
					
				val for1_inner_for2 = For(column, 
										Neg(j1), 
										width - (j2 - _1), 
										Statements( s ::: (app_index := app_index + _1) ))
					
				val for1_inner_for3 = For(column, 
										width - j2, 
										width - _1, 
										Statements( assert (column < Neg(j1)) ::: s ::: (app_index := app_index + _1)))
					
				val for1 = For(row, 
							_0, 
							Neg(i1) - _1, 
							Statements( assert (row < (height - i2)) :: for1_inner_for1 :: for1_inner_for2 :: for1_inner_for3 :: Nil ))
				
				// Note that the inner for loops for the second for are the same as that for the first one
				val for2 = For(row, 
							_0, 
							Neg(j1) - _1, 
							Statements( for1_inner_for1 :: for1_inner_for2 :: for1_inner_for3 :: Nil ))
				
				// Note that the inner for loops for the third for are the same as that for the first and second one
				val for3 = For(row, 
							height - i2, 
							height - _1, 
							Statements( assert (row >= Neg(i1)) :: for1_inner_for1 :: for1_inner_for2 :: for1_inner_for3 :: Nil ))
				
				val for4_inner = For(column, 
									_0, 
									width - _1,	
									Statements( s ::: (app_index := app_index + _1)))
									
				val for4 = For(row, 
							_0, 
							height - _1, 
							Statements( for4_inner :: Nil ))

				val if_else_stmt = IfElse((width > (j2 - j1)) and (height > (i2 - i1)),
									Statements( for1 :: for2 :: for3 :: Nil ),
									Statements( for4 :: Nil ))
				
				Statements( (app_index := _0) :: if_else_stmt :: Nil ) 
	}

	def FixLoop10RasterNoIndex = 
		rulefs {
		/*
			FixLoop10RasterNoIndex :
		    |[ @apply ~looptype window (i1..i2,j1..j2) loop ~s end loop; ]| -> 
		    |[ if width > j2 - j1 and height > i2 - i1 then
		         for row in 0..-i1-1 loop
		           assert row < height - i2;
		           for column in 0..-j1-1 loop
		             assert column < width - j2;
		             ~s
		           end loop;
		           for column in -j1..width-j2-1 loop
		             ~s
		           end loop;
		           for column in width-j2..width-1 loop
		             assert column >= -j1;
		             ~s
		           end loop;
		         end loop;
		         for row in -i1..height-i2-1 loop
		           for column in 0..-j1-1 loop
		             assert column < width - j2;
		             ~s
		           end loop;
		           for column in -j1..width-j2-1 loop
		             ~s
		           end loop;
		           for column in width-j2..width-1 loop
		             assert column >= -j1;
		             ~s
		           end loop;
		         end loop;
		         for row in height-i2..height-1 loop
		           assert row >= -i1;
		           for column in 0..-j1-1 loop
		             assert column < width - j2;
		             ~s
		           end loop;
		           for column in -j1..width-j2-1 loop
		             ~s
		           end loop;
		           for column in width-j2..width-1 loop
		             assert column >= -j1;
		             ~s
		           end loop;
		         end loop;
		       else
		         for row in 0..height-1 loop
		           for column in 0..width-1 loop
		             ~s
		           end loop;
		         end loop;
		       end if;
		    ]|   where(<debug> ["extreme window dimensions: ", i1, i2, j1 ,j2])
		*/
			case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>
				
				val for1_inner_for1 = For(column, 
										_0, 
										Sub(Neg(j1), _1), 
										Statements( Assert(column < (width - j2)) ::: s ))
										
				val for1_inner_for2 = For(column, 
										Neg(j1), 
										width - (j2 - _1), 
										s)
										
				val for1_inner_for3 = For(column, 
										width - j2, 
										width - _1, 
										Statements( Assert(column < Neg(j1)) ::: s))
				
				val for1 = For(row, 
							_0, 
							Neg(i1) - _1, 
							Statements( assert (row < (height - i2)) :: for1_inner_for1 :: for1_inner_for2 :: for1_inner_for3 :: Nil ))
				
				// Note that the inner for loops for the second for are the same as that for the first one
				val for2 = For(row, 
							Neg(i1), 
							height - (i2 - _1), 
							Statements( for1_inner_for1 :: for1_inner_for2 :: for1_inner_for3 :: Nil ))
				
				// Note that the inner for loops for the third for are the same as that for the first and second one
				val for3 = For(row, 
							height - i2, 
							height - _1, 
							Statements( assert (row >= Neg(i1)) :: for1_inner_for1 :: for1_inner_for2 :: for1_inner_for3 :: Nil))
				
				val if_true_part = Statements(for1 :: for2 :: for3 :: Nil)
				
				val for4 = For(row, 
							_0, 
							height - _1, 
							Statements( For(column, _0, width - _1, s) :: Nil ))

				val if_else_stmt = IfElse((width > (j2 - j1)) and (height > (i2 - i1)), 
									if_true_part, 
									Statements( for4 :: Nil ))
									
				Statements(if_else_stmt :: Nil) 
	}
	
	def FixLoop10BlockNoIndex = 
		rulefs {
		/*
			FixLoop10BlockNoIndex :
		    |[ @apply ~looptype window (i1..i2,j1..j2) loop ~s end loop; ]| -> 
		    |[ if width > j2 - j1 and height > i2 - i1 then
		         for row in 0..-i1-1 loop
		           assert row < height - i2;
		           for column in 0..-j1-1 loop
		             assert column < width - j2;
		             ~s
		           end loop;
		         end loop;
		         for row in 0..-i1-1 loop
		           assert row < height - i2;
		           for column in -j1..width-j2-1 loop
		             ~s
		           end loop;
		         end loop;
		         for row in 0..-i1-1 loop
		           assert row < height - i2;
		           for column in width-j2..width-1 loop
		             assert column >= -j1;
		             ~s
		           end loop;
		         end loop;
		         for row in -i1..height-i2-1 loop
		           for column in 0..-j1-1 loop
		             assert column < width - j2;
		             ~s
		           end loop;
		         end loop;
		         for row in -i1..height-i2-1 loop
		           for column in -j1..width-j2-1 loop
		             ~s
		           end loop;
		         end loop;
		         for row in -i1..height-i2-1 loop
		           for column in width-j2..width-1 loop
		             assert column >= -j1;
		             ~s
		           end loop;
		         end loop;
		         for row in height-i2..height-1 loop
		           assert row >= -i1;
		           for column in 0..-j1-1 loop
		             assert column < width - j2;
		             ~s
		           end loop;
		         end loop;
		         for row in height-i2..height-1 loop
		           assert row >= -i1;
		           for column in -j1..width-j2-1 loop
		             ~s
		           end loop;
		         end loop;
		         for row in height-i2..height-1 loop
		           assert row >= -i1;
		           for column in width-j2..width-1 loop
		             assert column >= -j1;
		             ~s
		           end loop;
		         end loop;
		       else
		         for row in 0..height-1 loop
		           for column in 0..width-1 loop
		             ~s
		           end loop;
		         end loop;
		       end if;
		    ]|   where(<debug> ["extreme window dimensions: ", i1, i2, j1 ,j2])
		*/
		case Statements(ApplyLoop(loopType, i1 : Int, i2 : Int, j1 : Int, j2 : Int, s) :: Nil) =>
			
				val for1_inner_for = For(column, 
										_0, 
										Neg(j1) - _1, 
										Statements( Assert(column < (width - j2)) ::: s))
										
				val for1 = For(row, 
							_0, 
							Neg(i1) - _1, 
							Statements( assert (row < (height - i2)) :: for1_inner_for :: Nil ))
		
				val for2_inner_for = For(column, 
										Neg(j1), 
										width - (j2 - _1), 
										s)
										
				val for2 = For(row, 
							_0, 
							Neg(i1) - _1, 
							Statements( assert (row < (height - i2)) :: for2_inner_for :: Nil ))
			
				val for3_inner_for = For(column, 
										width - j2, 
										width - _1, 
										Statements( assert (column >= Neg(j1)) ::: s ))
										
				val for3 = For(row, 
							_0, 
							Neg(i1) - _1, 
							Statements( assert (row < (height - i2)) :: for3_inner_for :: Nil ))

				val for4_inner_for = For(column, 
										_0, 
										Neg(j1) - _1, 
										Statements( assert (column < (width - j2)) ::: s ))
										
				val for4 = For(row, 
							Neg(i1), 
							height - (i2 - _1), 
							Statements( for4_inner_for :: Nil ))

				val for5_inner_for = For(column, 
										Neg(j1), 
										width - (j2 - _1), 
										s)
										
				val for5 = For(row, 
							Neg(i1), 
							height - (i2 - _1), 
							Statements( for5_inner_for :: Nil ))
				
				val for6_inner_for = For(column, 
										width - j2, 
										width - _1, 
										Statements( assert (column >= Neg(j1)) ::: s ))
										
				val for6 = For(row, 
							Neg(i1), 
							height - (i2 - _1), 
							Statements( for6_inner_for :: Nil ))				
				
				val for7_inner_for = For(column, 
										_0, 
										Neg(j1) - _1, 
										Statements( assert (column < (width - j2)) ::: s ))
										
				val for7 = For(row, 
							height - i2, 
							height - _1, 
							Statements( assert (row >= Neg(i1)) :: for7_inner_for :: Nil))					
				
				val for8_inner_for = For(column, 
										Neg(j1), 
										width - (j2 - _1), 
										s)
										
				val for8 = For(row, 
							height - i2, 
							height - _1, 
							Statements( assert (row >= Neg(i1)) :: for8_inner_for :: Nil))		
				
				val for9_inner_for = For(column, 
										width - j2, 
										width - _1, 
										Statements( assert (column >= Neg(j1)) ::: s ))
										
				val for9 = For(row, 
							height - i2, 
							height - _1, 
							Statements( assert (row >= Neg(i1)) :: for9_inner_for :: Nil ))		
				
				val if_true_part = Statements(for1 :: for2 :: for3 :: for4 :: for5 :: for6 :: for7 :: for8 :: for9 :: Nil)
				
				val for10_inner_for = For(column, 
										_0, 
										width - _1, 
										s)
										
				val for10 = For(row, 
								_0, 
								height - _1, 
								Statements(for10_inner_for :: Nil))

				// We need to maintain the use of brackets here because the operators are evaluated from left to
				// with no precedence
				val if_else_stmt = IfElse((width > (j2 - j1) and (height > (i2 - i1))),
										if_true_part,
										Statements(for10 :: Nil))
				
				Statements(if_else_stmt :: Nil) 
	}
	
	/**
	 *	Port of FixDefined from Apply Image_Matrix Stratego program
	 */
	def FixDefined = 
		rulefs {
				//	FixDefined :
    		//		|[ defined(x(e1..e2,e3..e4)) ]| -> 
    		//			|[ (row >= -e1) and (row < height - e2) and (column >= -e3) and (column < width - e4) ]|
			case Defined(x, Range1(e1, e2), Range1(e3, e4)) =>
				(row >= Neg(e1)) and (row < height - e2) and (column >= Neg(e3)) and (column < width - e4)
		}
	
	/**
	 *	Port of FixWindowsIndexBorder from Apply Image_Matrix Stratego program
	 */
	def FixWindowsIndexBorder = 
		rulefs {
			//	FixWindowsIndexBorder :
    		//		WindowAccessElement(x,row,col,rowrange,colrange,Border(t,e),looptype) ->
      		//			IfElseExp( |[ defined(x( ~row..~row, ~col..~col)) ]| , Subscript(x, |[ ~row * width + app_index + ~col ]| ), e)
			case WindowAccessElement1(x, row, col, rowrange, colrange, Border(t,e), looptype) =>
				IfElseExp(Defined(x, Range(row), Range(col)), Subscript(x, (row * width) + app_index + col), e)	
		}
		
	/**
	 *	Port of FixWindowsIndex from Apply Image_Matrix Stratego program
	 */
	def FixWindowsIndex = 
		rulefs {
			//	FixWindowsIndex :
    		//		WindowAccessElement(x,row,col,rowrange,colrange,type,looptype) ->
      		//			Subscript(x, |[ ~row * width + app_index + ~col ]| )
			//	FixWindowsIndex :
    		//		WindowAccessScalar(x,type,looptype) ->
      		//			Subscript (x, |[ app_index ]| )
			case WindowAccessElement1(x, row, col, rowrange, colrange, ttype, looptype) =>
				Subscript(x, (row * width) + app_index + col)
			case WindowAccessScalar1(x, ttype, looptype) =>
				Subscript(x, app_index) 
		}
	
	/**
	 *	Port of FixWindowsNoIndexBorder from Apply Image_Matrix Stratego program
	 */
	def FixWindowsNoIndexBorder = 
		rulefs {
			//	FixWindowsNoIndexBorder :
    		//		WindowAccessElement(x,r,c,rowrange,colrange,Border(t,e),looptype) ->
      		//			IfElseExp( |[ defined(x( ~r..~r, ~c..~c)) ]| , Subscript(x, |[ (row + ~r) * width + column + ~c ]| ), e)
			case WindowAccessElement1(x, r, c, rowrange, colrange, Border(t,e), looptype) =>
				IfElseExp(Defined(x, Range(r), Range(c)), 
					Subscript(x, ((row + r) * width) + column + c), 
					e)
		}
	
	/**
	 *	Port of FixWindowsNoIndex from Apply Image_Matrix Stratego program
	 */
	def FixWindowsNoIndex = 
		rulefs {
			//	FixWindowsNoIndex :
    		//		WindowAccessScalar(x,type,looptype) ->
      		//			Subscript (x, |[ row * width + column ]| )
  			//	FixWindowsNoIndex :
    		//		WindowAccessElement(x,r,c,rowrange,colrange,type,looptype) ->
      		//			Subscript(x, |[ (row + ~r) * width + column + ~c ]| )
			case WindowAccessScalar1(x, ttype, looptype) =>
				Subscript(x, (row * width) + column)
			case WindowAccessElement1(x, r, c, rowrange, colrange, ttype, looptype) =>
				Subscript(x, ((row + r) * width) + column + c)
		}
	
	/**
	 *	Port of FixWindowsArg from Apply Image_Matrix Stratego program
	 */
	def FixWindowsArg = 
		rulefs {
			// 	Cannot use CArray because variable name is not available.
  			// 	Instead, use Ada array with empty range list to denote
  			// 	undimensioned C array.
  			// 	FixWindowsArg :
    		//		Window(type) -> Array([""], type)
  			// 	FixWindowsArg :
    		// 		WindowArray(rowrange,colrange,type) -> Array([""], type)
			case Window(ttype) =>
				ConvertTTypeToTArgType(Array(List[TRange](), ttype))
			case WindowArray(rowrange, colrange, ttype) =>
				ConvertTTypeToTArgType(Array(List[TRange](), ttype))
		}
	
	/**
	 *	This method helps add some sugar to the expression of assert statements
	 */
	private def assert ( expression : TExp ) = Assert(expression)
}